Λ-λογισμός με απλούς τύπους
Ο λ-λογισμός με απλούς τύπους (\lambda^\to) είναι μια θεωρίας τύπων, είναι μια ερμηνεία τύπων του λ-λογισμού με ένα μοναδικό κατασκευαστή τύπων (type constructor): \to, ο οποίος κατασκευάζει τύπους συναρτήσεων. Είναι το κανονικό και το πιο απλό παράδειγμα λ-λογισμού με τύπους, και εμφανίζει πολλές επιθυμητές και ενδιαφέρουσες ιδιότητες.